(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Export Matrix.Mat.Matrix_Module.

Import ListNotations. (* 导入List库标记 *)

(* Mat类型矩阵定义，其依赖于三个变量分别是A,m,n，其中A为矩阵元素类型，m为矩阵的高度，n为矩阵的宽度 *)

Check Mat.

Print Mat. Check mat. Check mat_height. Check mat_width.

(* 创建一个矩阵 *)

(* 矩阵的创建函数mkMat，在利用二维表创建矩阵前需要验证该二维表的高度 *)

Definition dl:= [[1;5];[6;2]]. Check dl: list(list nat).

Lemma dl_height: height dl = 2.
Proof. simpl. reflexivity. Qed.

Lemma dl_width: width dl 2.
Proof. simpl. split. reflexivity. split. reflexivity. apply I. Qed.

Definition ma:= mkMat nat 2 2 dl dl_height dl_width.

Check ma:Mat nat 2 2 . Compute ma.

Check mkMat: forall (A : Set) (m n : nat) (mat : list (list A)), 
  height mat = m -> width mat n -> Mat A m n.

Lemma height_tmp1: height [[1;2];[3;4];[5;6]] = 3.
Proof.
  auto. Qed.

Lemma width_tmp1: width [[1;2];[3;4];[5;6]] 2.
Proof.
  simpl. auto. Qed.

Definition mat_tmp1:= mkMat nat 3 2 [[1;2];[3;4];[5;6]] height_tmp1 width_tmp1.

Check mat_tmp1.

(* 简化方法，对如常用尺寸矩阵如旋转矩阵皆为3×3，可专门定义一个生成3×3的矩阵生成函数 *)

Definition mb:= mkMat_2_2   1 2 3 4 . (* mkMat_2_2 为自定义的生成3×3的矩阵创建函数*)

Check mb.

Compute mb.  (* {|  mat := [[1; 2]; [3; 4]];
                    mat_height := eq_refl; 
                    mat_width := mkMat_2_2_cond2 nat 1 2 3 4 |} *)

(* 矩阵运算以及转置函数 *)


(* 矩阵的加减法函数 *)

Definition Madd:= @matrix_each nat plus . (* 矩阵加法 *)
Arguments Madd{m}{n}. Check Madd.

Compute Madd ma mb.
(* [[2; 7]; [9; 6]] *)


Definition Msub:= @matrix_each nat minus. (* 矩阵减法 *)
Arguments Msub {m}{n}. Check Msub.

Compute Msub ma mb.
(* [[0; 3]; [3; 0]] *)

(* 矩阵的转置函数 *)

Definition Mtrans:= @trans nat 0.
Arguments Mtrans {m}{n}.

Check Mtrans. (* 矩阵转置 *)

Compute Mtrans mb.

(* [[1; 3]; [2; 4]]; *)

(* 矩阵的乘法函数 *)

Definition Mmult:=@matrix_mul nat 0 plus mult.
Arguments Mmult{m}{n}{p}.

Compute Mmult ma mb.

(* [[16; 22]; [12; 20]]; *)

Lemma Madd_comm: Madd ma mb === Madd mb ma.
Proof. unfold Madd,matrix_each,mat_each,ma,mb,M_eq.
  simpl. reflexivity. Qed.

Lemma Madd_comm':(forall a b : nat, a + b = b + a)-> Madd ma mb === Madd mb ma.
Proof. apply matrix_comm. Qed.





